Library triangle_centers_def
Require Import PointsETC.
Section Triangle.
Context `{M:triangle_theory}.
Definition is_center_function f:=
(∃ n, ∀ t a b c, f (t×a) (t×b) (t×c) = t^n× f a b c) ∧
(∀ a b c, f a b c = f a c b).
Definition h_x_3 a b c := a^2*(a^2-b^2-c^2).
Lemma h_x_3_ok : is_center_function h_x_3.
Proof.
unfold is_center_function.
split.
∃ 4%nat.
intros.
unfold h_x_3;simpl.
ring.
intros;unfold h_x_3;ring.
Qed.
End Triangle.
Section Triangle.
Context `{M:triangle_theory}.
Definition is_center_function f:=
(∃ n, ∀ t a b c, f (t×a) (t×b) (t×c) = t^n× f a b c) ∧
(∀ a b c, f a b c = f a c b).
Definition h_x_3 a b c := a^2*(a^2-b^2-c^2).
Lemma h_x_3_ok : is_center_function h_x_3.
Proof.
unfold is_center_function.
split.
∃ 4%nat.
intros.
unfold h_x_3;simpl.
ring.
intros;unfold h_x_3;ring.
Qed.
End Triangle.